En el proyecto se han implementado las ideas propuestas en \cite{flops2010} para la obtención de casos de prueba para bases de datos SQL y se han extendido las mismas para dar solución a consultas existenciales anidadas \cite{prole2012}. El desarrollo se ha concretado en tres módulos principales: parser, generador de fórmulas y traductor a lenguajes específicos o resolutores, cuyas principales características mostramos a continuación.
\begin{itemize}
\item \emph{Parser}

Hemos desarrollado un analizador sintáctico de un subconjunto de SQL (ver sección \ref{sec:ambito} y apéndice \ref{app:grammar}). Esto nos permite obtener la estructura de la base de datos que deseamos estudiar a partir de su definición en lenguaje SQL.

\item \emph{Generador de fórmulas}

A partir de la representación de la base de datos obtenida por el parser y aplicando las técnicas propuestas en \cite{flops2010} y \cite{prole2012} generamos las restricciones que deben cumplir los casos de prueba. Estas restricciones se generan en un formato interno, que nos permite posteriormente traducirlas a diversos lenguajes de programación con restricciones.

\item \emph{Generador de código MiniZinc}

Nuestra herramienta traduce las fórmulas generadas en el módulo anterior a código MiniZinc \cite{MiniZinc}. El código generado (ver apéndice \ref{app:sec:output}) se divide en la declaración de las variables, la definición de las restricciones, la llamada al resolutor y el formato de salida. Este código será posteriormente ejecutado en un resolutor para encontrar, si existiera, un caso de prueba. 

Actualmente la salida del resolutor tiene un formato compatible con SQL (ver resultado en la página \pageref{resultado}), de forma que se puede introducir fácilmente el caso de prueba generado en la base de datos.
\end{itemize}